Nuprl Lemma : ma-feasible-bframe 11,40

A:MsgA, l:IdLnk, k:Knd, s:A.state, v:A.da(k).
ma-frame-compat(A;A)
 (A.bframe(k sends on l))
 (filter(ms.mlnk(ms) = l;A.sends(k,s,v)) = []  (A.Msg List)) 
latex


Definitions<ab>, s = t, filter(P;l), M.sends(k,s,v), a = b, [], M.Msg, M.V(k), MsgA, Valtype(da;k), ma-frame-compat(A;B), M.rframe(A.pre p for a), M.frame(k affects x), M.aframe(k affects x), M.rframe(A.effect f of k on y), M.sframe(k sends <l,tg>), M.bframe(k sends on l), M.rframe(A.sends tfL of k on l), M.state, M.da(a), xdom(f). v=f(x  P(x;v), State(ds), x  dom(f), product-deq(A;B;a;b), IdLnkDeq, a:A fp B(a), IdDeq, t.1, Top, type List, f(x)?z, KindDeq, rcv(l,tg), t.2, xt(x), x.A(x), Type, Void, S  T, x:AB(x), IdLnk, Knd, x:A  B(x), Id, t  T, b, P & Q, x:AB(x), A, P  Q, False
LemmasIdLnk wf, Knd wf, pi2 wf, rcv wf, Kind-deq wf, fpf-cap wf, top wf, pi1 wf, id-deq wf, Id wf, fpf-trivial-subtype-top, idlnk-deq wf, product-deq wf, fpf-dom wf, assert wf, ma-da wf, subtype rel self, ma-msg wf, ma-send-val-nil, msga wf, ma-st wf, ma-frame-compat wf, ma-bframe wf, not wf

origin